es:event_system{i:l}, i,x:Id, T:Type.
es-dtype(es; i; x; T)
 (t:rationals. es-init-elapsed(es; i; t)(x) = es-initially(es; i; x)  T) 

latex

Definitions	t  T, P  Q, P  Q, x:A. B(x), Id, b, es-T(es), es-isconst(es; i; x), x:A  B(x), event_system{i:l}, x:AB(x), es-dtype(es; i; x; T), es-initially(es; i; x), es-init-elapsed(es; i; t), Type, <a, b>, s = t, es-vartype(es; i; x), rationals, es_init(es), f(a), constant_function(f; A; B), , es_vartype(es; i; x), es_state(es; i), prop{i:l}, sqequal(s; t), guard(T), sq_type(T), #$n
Lemmas	es-vartype wf, es init wf, es state wf, int inc rationals, rationals wf, es-dtype wf, event system wf, assert wf, Id wf